i:top, L:(top List), A:top.
sqequal(R-da(Rall(L; x.A(x)); i);
sqequal(reduce((x,da. fpf-join(Kind-deq; R-da(A(x); i); da)); fpf-empty; L)) 

latex

Definitions	Y, t  T, map(f; as), reduce(f; k; as), Rall(L; x.R(x)), top, x:A. B(x)
Lemmas	top wf, map wf, R-da-Rlist